|
In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term. Functional predicates are also sometimes called ''mappings'', but that term has other meanings as well. In a model, a function symbol will be modelled by a function. Specifically, the symbol ''F'' in a formal language is a functional symbol if, given any symbol ''X'' representing an object in the language, ''F''(''X'') is again a symbol representing an object in that language. In typed logic, ''F'' is a functional symbol with ''domain'' type T and ''codomain'' type U if, given any symbol ''X'' representing an object of type T, ''F''(''X'') is a symbol representing an object of type U. One can similarly define function symbols of more than one variable, analogous to functions of more than one variable; a function symbol in zero variables is simply a constant symbol. Now consider a model of the formal language, with the types T and U modelled by sets () and () and each symbol ''X'' of type T modelled by an element () in (). Then ''F'' can be modelled by the set : which is simply a function with domain () and codomain (). It is a requirement of a consistent model that () = () whenever () = (). ==Introducing new function symbols== In a treatment of predicate logic that allows one to introduce new predicate symbols, one will also want to be able to introduce new function symbols. Given the function symbols ''F'' and ''G'', one can introduce a new function symbol ''F'' ∘ ''G'', the ''composition'' of ''F'' and ''G'', satisfying (''F'' ∘ ''G'')(''X'') = ''F''(''G''(''X'')), for all ''X''. Of course, the right side of this equation doesn't make sense in typed logic unless the domain type of ''F'' matches the codomain type of ''G'', so this is required for the composition to be defined. One also gets certain function symbols automatically. In untyped logic, there is an ''identity predicate'' id that satisfies id(''X'') = ''X'' for all ''X''. In typed logic, given any type T, there is an identity predicate idT with domain and codomain type T; it satisfies idT(''X'') = ''X'' for all ''X'' of type T. Similarly, if T is a subtype of U, then there is an inclusion predicate of domain type T and codomain type U that satisfies the same equation; there are additional function symbols associated with other ways of constructing new types out of old ones. Additionally, one can define functional predicates after proving an appropriate theorem. (If you're working in a formal system that doesn't allow you to introduce new symbols after proving theorems, then you will have to use relation symbols to get around this, as in the next section.) Specifically, if you can prove that for every ''X'' (or every ''X'' of a certain type), there exists a unique ''Y'' satisfying some condition ''P'', then you can introduce a function symbol ''F'' to indicate this. Note that ''P'' will itself be a relational predicate involving both ''X'' and ''Y''. So if there is such a predicate ''P'' and a theorem: : For all ''X'' of type T, for some unique ''Y'' of type U, ''P''(''X'',''Y''), then you can introduce a function symbol ''F'' of domain type T and codomain type U that satisfies: : For all ''X'' of type T, for all ''Y'' of type U, ''P''(''X'',''Y'') if and only if ''Y'' = ''F''(''X''). 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Functional predicate」の詳細全文を読む スポンサード リンク
|